$\forall$${\it es}$:event\_system\{i:l\}, $i$:Id, ${\it ds}_{1}$,${\it ds}_{2}$:fpf(Id; $x$.Type).
\\[0ex]fpf{-}sub(Id; $x$.Type; id{-}deq; ${\it ds}_{2}$; ${\it ds}_{1}$)
\\[0ex]$\Rightarrow$ ($\forall$$x$:Id. subtype\_rel(es{-}vartype(${\it es}$; $i$; $x$); fpf{-}cap(${\it ds}_{1}$; id{-}deq; $x$; top)))
\\[0ex]$\Rightarrow$ subtype\_rel(es{-}state(${\it es}$; $i$); decl{-}state(${\it ds}_{2}$))